0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 188 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 22 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 244 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 23 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
GOALD_IN_G(s(T11)) → U8_G(T11, s2tA_in_ga(T11, X29))
GOALD_IN_G(s(T11)) → S2TA_IN_GA(T11, X29)
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → U1_GA(T19, X64, X65, s2tA_in_ga(T19, X64))
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → S2TA_IN_GA(T19, X64)
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → U2_GA(T25, X94, X95, s2tA_in_ga(T25, X95))
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → S2TA_IN_GA(T25, X95)
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → U3_GA(T31, X124, X125, s2tA_in_ga(T31, X124))
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → S2TA_IN_GA(T31, X124)
GOALD_IN_G(s(T11)) → U9_G(T11, s2tA_in_ga(T11, T13))
U9_G(T11, s2tA_out_ga(T11, T13)) → U10_G(T11, tappendC_in_gaaa(T13, X30, X4, X5))
U9_G(T11, s2tA_out_ga(T11, T13)) → TAPPENDC_IN_GAAA(T13, X30, X4, X5)
TAPPENDC_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → U6_GAAA(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
TAPPENDC_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → TAPPENDB_IN_GAA(T50, X245, X246)
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_GAA(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDB_IN_GAA(T86, X334, X335)
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_GAA(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDB_IN_GAA(T96, X359, X360)
TAPPENDC_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → U7_GAAA(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
TAPPENDC_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → TAPPENDB_IN_GAA(T101, X391, X392)
GOALD_IN_G(s(T106)) → U11_G(T106, s2tA_in_ga(T106, X421))
GOALD_IN_G(s(T106)) → U12_G(T106, s2tA_in_ga(T106, T108))
U12_G(T106, s2tA_out_ga(T106, T108)) → U13_G(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U12_G(T106, s2tA_out_ga(T106, T108)) → TAPPENDB_IN_GAA(node(nil, X420, T108), X4, X5)
GOALD_IN_G(s(T114)) → U14_G(T114, s2tA_in_ga(T114, X457))
GOALD_IN_G(s(T114)) → U15_G(T114, s2tA_in_ga(T114, T116))
U15_G(T114, s2tA_out_ga(T114, T116)) → U16_G(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U15_G(T114, s2tA_out_ga(T114, T116)) → TAPPENDB_IN_GAA(node(T116, X458, nil), X4, X5)
GOALD_IN_G(s(T122)) → U17_G(T122, tappendC_in_gaaa(nil, X485, X4, X5))
GOALD_IN_G(s(T122)) → TAPPENDC_IN_GAAA(nil, X485, X4, X5)
GOALD_IN_G(0) → U18_G(tappendB_in_gaa(nil, X4, X5))
GOALD_IN_G(0) → TAPPENDB_IN_GAA(nil, X4, X5)
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
GOALD_IN_G(s(T11)) → U8_G(T11, s2tA_in_ga(T11, X29))
GOALD_IN_G(s(T11)) → S2TA_IN_GA(T11, X29)
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → U1_GA(T19, X64, X65, s2tA_in_ga(T19, X64))
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → S2TA_IN_GA(T19, X64)
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → U2_GA(T25, X94, X95, s2tA_in_ga(T25, X95))
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → S2TA_IN_GA(T25, X95)
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → U3_GA(T31, X124, X125, s2tA_in_ga(T31, X124))
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → S2TA_IN_GA(T31, X124)
GOALD_IN_G(s(T11)) → U9_G(T11, s2tA_in_ga(T11, T13))
U9_G(T11, s2tA_out_ga(T11, T13)) → U10_G(T11, tappendC_in_gaaa(T13, X30, X4, X5))
U9_G(T11, s2tA_out_ga(T11, T13)) → TAPPENDC_IN_GAAA(T13, X30, X4, X5)
TAPPENDC_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → U6_GAAA(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
TAPPENDC_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → TAPPENDB_IN_GAA(T50, X245, X246)
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_GAA(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDB_IN_GAA(T86, X334, X335)
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_GAA(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDB_IN_GAA(T96, X359, X360)
TAPPENDC_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → U7_GAAA(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
TAPPENDC_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → TAPPENDB_IN_GAA(T101, X391, X392)
GOALD_IN_G(s(T106)) → U11_G(T106, s2tA_in_ga(T106, X421))
GOALD_IN_G(s(T106)) → U12_G(T106, s2tA_in_ga(T106, T108))
U12_G(T106, s2tA_out_ga(T106, T108)) → U13_G(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U12_G(T106, s2tA_out_ga(T106, T108)) → TAPPENDB_IN_GAA(node(nil, X420, T108), X4, X5)
GOALD_IN_G(s(T114)) → U14_G(T114, s2tA_in_ga(T114, X457))
GOALD_IN_G(s(T114)) → U15_G(T114, s2tA_in_ga(T114, T116))
U15_G(T114, s2tA_out_ga(T114, T116)) → U16_G(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U15_G(T114, s2tA_out_ga(T114, T116)) → TAPPENDB_IN_GAA(node(T116, X458, nil), X4, X5)
GOALD_IN_G(s(T122)) → U17_G(T122, tappendC_in_gaaa(nil, X485, X4, X5))
GOALD_IN_G(s(T122)) → TAPPENDC_IN_GAAA(nil, X485, X4, X5)
GOALD_IN_G(0) → U18_G(tappendB_in_gaa(nil, X4, X5))
GOALD_IN_G(0) → TAPPENDB_IN_GAA(nil, X4, X5)
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDB_IN_GAA(T96, X359, X360)
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDB_IN_GAA(T86, X334, X335)
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
TAPPENDB_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDB_IN_GAA(T96, X359, X360)
TAPPENDB_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDB_IN_GAA(T86, X334, X335)
TAPPENDB_IN_GAA(node(T93, T96)) → TAPPENDB_IN_GAA(T96)
TAPPENDB_IN_GAA(node(T86, T85)) → TAPPENDB_IN_GAA(T86)
From the DPs we obtained the following set of size-change graphs:
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → S2TA_IN_GA(T25, X95)
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → S2TA_IN_GA(T19, X64)
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → S2TA_IN_GA(T31, X124)
goalD_in_g(s(T11)) → U8_g(T11, s2tA_in_ga(T11, X29))
s2tA_in_ga(s(T19), node(X64, X65, X64)) → U1_ga(T19, X64, X65, s2tA_in_ga(T19, X64))
s2tA_in_ga(s(T25), node(nil, X94, X95)) → U2_ga(T25, X94, X95, s2tA_in_ga(T25, X95))
s2tA_in_ga(s(T31), node(X124, X125, nil)) → U3_ga(T31, X124, X125, s2tA_in_ga(T31, X124))
s2tA_in_ga(s(T37), node(nil, X145, nil)) → s2tA_out_ga(s(T37), node(nil, X145, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T31, X124, X125, s2tA_out_ga(T31, X124)) → s2tA_out_ga(s(T31), node(X124, X125, nil))
U2_ga(T25, X94, X95, s2tA_out_ga(T25, X95)) → s2tA_out_ga(s(T25), node(nil, X94, X95))
U1_ga(T19, X64, X65, s2tA_out_ga(T19, X64)) → s2tA_out_ga(s(T19), node(X64, X65, X64))
U8_g(T11, s2tA_out_ga(T11, X29)) → goalD_out_g(s(T11))
goalD_in_g(s(T11)) → U9_g(T11, s2tA_in_ga(T11, T13))
U9_g(T11, s2tA_out_ga(T11, T13)) → U10_g(T11, tappendC_in_gaaa(T13, X30, X4, X5))
tappendC_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendC_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendC_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendC_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendC_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U6_gaaa(T50, X244, X245, X246, tappendB_in_gaa(T50, X245, X246))
tappendB_in_gaa(nil, X260, X260) → tappendB_out_gaa(nil, X260, X260)
tappendB_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendB_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendB_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendB_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendB_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U4_gaa(T86, T84, T85, X334, X335, tappendB_in_gaa(T86, X334, X335))
tappendB_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U5_gaa(T93, T94, T96, X359, X360, tappendB_in_gaa(T96, X359, X360))
U5_gaa(T93, T94, T96, X359, X360, tappendB_out_gaa(T96, X359, X360)) → tappendB_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U4_gaa(T86, T84, T85, X334, X335, tappendB_out_gaa(T86, X334, X335)) → tappendB_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U6_gaaa(T50, X244, X245, X246, tappendB_out_gaa(T50, X245, X246)) → tappendC_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendC_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U7_gaaa(T101, X390, X391, X392, tappendB_in_gaa(T101, X391, X392))
U7_gaaa(T101, X390, X391, X392, tappendB_out_gaa(T101, X391, X392)) → tappendC_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U10_g(T11, tappendC_out_gaaa(T13, X30, X4, X5)) → goalD_out_g(s(T11))
goalD_in_g(s(T106)) → U11_g(T106, s2tA_in_ga(T106, X421))
U11_g(T106, s2tA_out_ga(T106, X421)) → goalD_out_g(s(T106))
goalD_in_g(s(T106)) → U12_g(T106, s2tA_in_ga(T106, T108))
U12_g(T106, s2tA_out_ga(T106, T108)) → U13_g(T106, tappendB_in_gaa(node(nil, X420, T108), X4, X5))
U13_g(T106, tappendB_out_gaa(node(nil, X420, T108), X4, X5)) → goalD_out_g(s(T106))
goalD_in_g(s(T114)) → U14_g(T114, s2tA_in_ga(T114, X457))
U14_g(T114, s2tA_out_ga(T114, X457)) → goalD_out_g(s(T114))
goalD_in_g(s(T114)) → U15_g(T114, s2tA_in_ga(T114, T116))
U15_g(T114, s2tA_out_ga(T114, T116)) → U16_g(T114, tappendB_in_gaa(node(T116, X458, nil), X4, X5))
U16_g(T114, tappendB_out_gaa(node(T116, X458, nil), X4, X5)) → goalD_out_g(s(T114))
goalD_in_g(s(T122)) → U17_g(T122, tappendC_in_gaaa(nil, X485, X4, X5))
U17_g(T122, tappendC_out_gaaa(nil, X485, X4, X5)) → goalD_out_g(s(T122))
goalD_in_g(0) → U18_g(tappendB_in_gaa(nil, X4, X5))
U18_g(tappendB_out_gaa(nil, X4, X5)) → goalD_out_g(0)
S2TA_IN_GA(s(T25), node(nil, X94, X95)) → S2TA_IN_GA(T25, X95)
S2TA_IN_GA(s(T19), node(X64, X65, X64)) → S2TA_IN_GA(T19, X64)
S2TA_IN_GA(s(T31), node(X124, X125, nil)) → S2TA_IN_GA(T31, X124)
S2TA_IN_GA(s(T25)) → S2TA_IN_GA(T25)
From the DPs we obtained the following set of size-change graphs: